So, for people who can't, if the general recording mechanism doesn't work, let me screen share.

There we go.

The DPLL procedure.

We have the algorithm here, but I would rather like to show it to you in the form of an example

first.

So what's happening here?

Sorry.

It hopped.

Right.

So we have a clause set.

This one here.

And we have two rules.

One is called unit propagation, UP.

We see we have a unit clause here, namely, R true.

What we can do with this is essentially just propagate this by getting rid of doing clause

simplification.

We have an R true here, so we can get rid of the R false, because it's never going to

be false.

So I can shorten this, and I can get rid of all the clauses which contain an R true, which

in this case, there aren't any.

So we have P true, Q true.

That's the initial part of this one.

We have P false, Q false left over.

And we have P true and Q false.

That's the last clause here.

We can get rid of the unit and of all and do clause simplification with it.

That gives us a shorter clause set.

So that simplified our system, and we can't do anything because we don't have any units

left over.

So what we do is we have to use a different rule, the so-called splitting rule, which

basically allows, which basically takes a clause and takes a variable.

In this case, we take the P. And on one branch, we set it to false, which gives us a new unit,

which we can then use for simplifying.

If we have a P to false, we can simplify this clause to Q true.

We have a P false or Q false.

With a P false, we can drop this because this is never going to contribute to an empty clause.

And we have the P true, Q false, which we actually simplify to this.

We have two more.

We've created two units in this, and the unit propagation rule actually gives us the empty

clause.

On the other branch, we have a P true, which gives us, after clause simplification, a Q

false.

We can do a unit.

We can do a unit propagation, and actually that makes the clause set empty, which is

different from an empty clause.

An empty clause gives us unsatisfiability.

That's essentially a proof.

And if we have an empty clause set, that actually gives us a satisfying clause.

So we return all the decisions we've made, namely R goes to true, P goes to true, and

Q goes to false.